

LEMMA

If x is externally connected to y and y is a tangential proper part of z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (tpp y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (ec c481600 c481599)) v (~ (tpp c481599 c481598))) v (~ (p c481598 c481600)))


> hypdisj
=============================
Step 3

? (~ (p c481598 c481600))

1. (tpp c481599 c481598)
2. (ec c481600 c481599)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var70 c481598)
|
|1. (p c481598 c481600)
|2. (tpp c481599 c481598)
|3. (ec c481600 c481599)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var73 c481598)
||
||1. (~ (c Var70 c481598))
||2. (p c481598 c481600)
||3. (tpp c481599 c481598)
||4. (ec c481600 c481599)
||
||> ((p Z X) <-- (~ (c (f476547 Z X Y) Z)))
||=============================
||Step 6
||
||? (~ (c (f476547 Var73 c481598 Var76) Var73))
||
||1. (~ (p Var73 c481598))
||2. (~ (c Var70 c481598))
||3. (p c481598 c481600)
||4. (tpp c481599 c481598)
||5. (ec c481600 c481599)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 7
|||
|||? (p Var73 Var79)
|||
|||1. (c (f476547 Var73 c481598 Var76) Var73)
|||2. (~ (p Var73 c481598))
|||3. (~ (c Var70 c481598))
|||4. (p c481598 c481600)
|||5. (tpp c481599 c481598)
|||6. (ec c481600 c481599)
|||
|||> ((p X Y) <-- (pp X Y))
|||=============================
|||Step 8
|||
|||? (pp Var73 Var79)
|||
|||1. (~ (p Var73 Var79))
|||2. (c (f476547 Var73 c481598 Var76) Var73)
|||3. (~ (p Var73 c481598))
|||4. (~ (c Var70 c481598))
|||5. (p c481598 c481600)
|||6. (tpp c481599 c481598)
|||7. (ec c481600 c481599)
|||
|||> ((pp X Y) <-- (tpp X Y))
|||=============================
|||Step 9
|||
|||? (tpp Var73 Var79)
|||
|||1. (~ (pp Var73 Var79))
|||2. (~ (p Var73 Var79))
|||3. (c (f476547 Var73 c481598 Var76) Var73)
|||4. (~ (p Var73 c481598))
|||5. (~ (c Var70 c481598))
|||6. (p c481598 c481600)
|||7. (tpp c481599 c481598)
|||8. (ec c481600 c481599)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (c (f476547 c481599 c481598 Var76) c481598))
||
||1. (c (f476547 c481599 c481598 Var76) c481599)
||2. (~ (p c481599 c481598))
||3. (~ (c Var70 c481598))
||4. (p c481598 c481600)
||5. (tpp c481599 c481598)
||6. (ec c481600 c481599)
||
||> ((~ (c (f476547 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 11
||
||? (~ (p c481599 c481598))
||
||1. (c (f476547 c481599 c481598 Var76) c481598)
||2. (c (f476547 c481599 c481598 Var76) c481599)
||3. (~ (p c481599 c481598))
||4. (~ (c Var70 c481598))
||5. (p c481598 c481600)
||6. (tpp c481599 c481598)
||7. (ec c481600 c481599)
||
||> hyp
|=============================
|Step 12
|
|? (c (f476547 c481599 Var91 Var92) c481599)
|
|1. (~ (c (f476547 c481599 Var91 Var92) c481598))
|2. (p c481598 c481600)
|3. (tpp c481599 c481598)
|4. (ec c481600 c481599)
|
|> ((c (f476547 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 13
|
|? (~ (p c481599 Var91))
|
|1. (~ (c (f476547 c481599 Var91 Var92) c481599))
|2. (~ (c (f476547 c481599 Var91 Var92) c481598))
|3. (p c481598 c481600)
|4. (tpp c481599 c481598)
|5. (ec c481600 c481599)
|
|> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
||=============================
||Step 14
||
||? (p c481599 Var95)
||
||1. (p c481599 Var91)
||2. (~ (c (f476547 c481599 Var91 Var92) c481599))
||3. (~ (c (f476547 c481599 Var91 Var92) c481598))
||4. (p c481598 c481600)
||5. (tpp c481599 c481598)
||6. (ec c481600 c481599)
||
||> ((p Z X) <-- (~ (c (f476547 Z X Y) Z)))
||=============================
||Step 15
||
||? (~ (c (f476547 c481599 c481599 Var98) c481599))
||
||1. (~ (p c481599 c481599))
||2. (p c481599 Var91)
||3. (~ (c (f476547 c481599 Var91 Var92) c481599))
||4. (~ (c (f476547 c481599 Var91 Var92) c481598))
||5. (p c481598 c481600)
||6. (tpp c481599 c481598)
||7. (ec c481600 c481599)
||
||> ((~ (c (f476547 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 16
||
||? (~ (p c481599 c481599))
||
||1. (c (f476547 c481599 c481599 Var98) c481599)
||2. (~ (p c481599 c481599))
||3. (p c481599 Var91)
||4. (~ (c (f476547 c481599 Var91 Var92) c481599))
||5. (~ (c (f476547 c481599 Var91 Var92) c481598))
||6. (p c481598 c481600)
||7. (tpp c481599 c481598)
||8. (ec c481600 c481599)
||
||> hyp
|=============================
|Step 17
|
|? (~ (o Var91 c481599))
|
|1. (p c481599 Var91)
|2. (~ (c (f476547 c481599 Var91 Var92) c481599))
|3. (~ (c (f476547 c481599 Var91 Var92) c481598))
|4. (p c481598 c481600)
|5. (tpp c481599 c481598)
|6. (ec c481600 c481599)
|
|> ((~ (o X Y)) <-- (ec X Y))
|=============================
|Step 18
|
|? (ec Var91 c481599)
|
|1. (o Var91 c481599)
|2. (p c481599 Var91)
|3. (~ (c (f476547 c481599 Var91 Var92) c481599))
|4. (~ (c (f476547 c481599 Var91 Var92) c481598))
|5. (p c481598 c481600)
|6. (tpp c481599 c481598)
|7. (ec c481600 c481599)
|
|> hyp
=============================
Step 19

? (~ (c (f476547 c481599 c481600 Var92) c481600))

1. (p c481598 c481600)
2. (tpp c481599 c481598)
3. (ec c481600 c481599)

> ((~ (c (f476547 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 20

? (~ (p c481599 c481600))

1. (c (f476547 c481599 c481600 Var92) c481600)
2. (p c481598 c481600)
3. (tpp c481599 c481598)
4. (ec c481600 c481599)

> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
|=============================
|Step 21
|
|? (p c481599 Var109)
|
|1. (p c481599 c481600)
|2. (c (f476547 c481599 c481600 Var92) c481600)
|3. (p c481598 c481600)
|4. (tpp c481599 c481598)
|5. (ec c481600 c481599)
|
|> ((p Z X) <-- (~ (c (f476547 Z X Y) Z)))
|=============================
|Step 22
|
|? (~ (c (f476547 c481599 c481599 Var112) c481599))
|
|1. (~ (p c481599 c481599))
|2. (p c481599 c481600)
|3. (c (f476547 c481599 c481600 Var92) c481600)
|4. (p c481598 c481600)
|5. (tpp c481599 c481598)
|6. (ec c481600 c481599)
|
|> ((~ (c (f476547 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 23
|
|? (~ (p c481599 c481599))
|
|1. (c (f476547 c481599 c481599 Var112) c481599)
|2. (~ (p c481599 c481599))
|3. (p c481599 c481600)
|4. (c (f476547 c481599 c481600 Var92) c481600)
|5. (p c481598 c481600)
|6. (tpp c481599 c481598)
|7. (ec c481600 c481599)
|
|> hyp
=============================
Step 24

? (~ (o c481600 c481599))

1. (p c481599 c481600)
2. (c (f476547 c481599 c481600 Var92) c481600)
3. (p c481598 c481600)
4. (tpp c481599 c481598)
5. (ec c481600 c481599)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 25

? (ec c481600 c481599)

1. (o c481600 c481599)
2. (p c481599 c481600)
3. (c (f476547 c481599 c481600 Var92) c481600)
4. (p c481598 c481600)
5. (tpp c481599 c481598)
6. (ec c481600 c481599)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c486829 c486828)) v (pp c486829 c486828))


> hypdisj
=============================
Step 3

? (pp c486829 c486828)

1. (tpp c486829 c486828)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c486829 c486828)

1. (~ (pp c486829 c486828))
2. (tpp c486829 c486828)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c492114 c492113)) v (p c492114 c492113))


> hypdisj
=============================
Step 3

? (p c492114 c492113)

1. (pp c492114 c492113)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c492114 c492113)

1. (~ (p c492114 c492113))
2. (pp c492114 c492113)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c497457 c497456)) v (~ (c c497455 c497457))) v (c c497455 c497456))


> hypdisj
=============================
Step 3

? (c c497455 c497456)

1. (c c497455 c497457)
2. (p c497457 c497456)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c497456)
|
|1. (~ (c c497455 c497456))
|2. (c c497455 c497457)
|3. (p c497457 c497456)
|
|> hyp
=============================
Step 5

? (c c497455 c497457)

1. (~ (c c497455 c497456))
2. (c c497455 c497457)
3. (p c497457 c497456)

> hyp


LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c502954 c502953)) v (c c502954 c502953))


> hypdisj
=============================
Step 3

? (c c502954 c502953)

1. (ec c502954 c502953)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c502954 c502953)

1. (~ (c c502954 c502953))
2. (ec c502954 c502953)

> hyp


LEMMA

From ec(x,y) and tpp(y,z), x is connected to z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (tpp y z)) => (c x z)))))


> revsk
=============================
Step 2

? (((~ (ec c508509 c508508)) v (~ (tpp c508508 c508507))) v (c c508509 c508507))


> hypdisj
=============================
Step 3

? (c c508509 c508507)

1. (tpp c508508 c508507)
2. (ec c508509 c508508)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var30 c508507)
|
|1. (~ (c c508509 c508507))
|2. (tpp c508508 c508507)
|3. (ec c508509 c508508)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 5
|
|? (pp Var30 c508507)
|
|1. (~ (p Var30 c508507))
|2. (~ (c c508509 c508507))
|3. (tpp c508508 c508507)
|4. (ec c508509 c508508)
|
|> ((pp X Y) <-- (tpp X Y))
|=============================
|Step 6
|
|? (tpp Var30 c508507)
|
|1. (~ (pp Var30 c508507))
|2. (~ (p Var30 c508507))
|3. (~ (c c508509 c508507))
|4. (tpp c508508 c508507)
|5. (ec c508509 c508508)
|
|> hyp
=============================
Step 7

? (c c508509 c508508)

1. (~ (c c508509 c508507))
2. (tpp c508508 c508507)
3. (ec c508509 c508508)

> ((c X Y) <-- (ec X Y))
=============================
Step 8

? (ec c508509 c508508)

1. (~ (c c508509 c508508))
2. (~ (c c508509 c508507))
3. (tpp c508508 c508507)
4. (ec c508509 c508508)

> hyp


LEMMA

Since x is connected to z, either ec(x,z) or x overlaps z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (tpp y z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? (((~ (ec c514220 c514219)) v (~ (tpp c514219 c514218))) v ((ec c514220 c514218) v (o c514220 c514218)))


> hypdisj
=============================
Step 3

? (o c514220 c514218)

1. (~ (ec c514220 c514218))
2. (tpp c514219 c514218)
3. (ec c514220 c514219)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c514220 c514218)
|
|1. (~ (o c514220 c514218))
|2. (~ (ec c514220 c514218))
|3. (tpp c514219 c514218)
|4. (ec c514220 c514219)
|
|> ((c X Z) <-- (ec X Y) (tpp Y Z))
||=============================
||Step 5
||
||? (ec c514220 Var29)
||
||1. (~ (c c514220 c514218))
||2. (~ (o c514220 c514218))
||3. (~ (ec c514220 c514218))
||4. (tpp c514219 c514218)
||5. (ec c514220 c514219)
||
||> hyp
|=============================
|Step 6
|
|? (tpp c514219 c514218)
|
|1. (~ (c c514220 c514218))
|2. (~ (o c514220 c514218))
|3. (~ (ec c514220 c514218))
|4. (tpp c514219 c514218)
|5. (ec c514220 c514219)
|
|> hyp
=============================
Step 7

? (~ (ec c514220 c514218))

1. (~ (o c514220 c514218))
2. (~ (ec c514220 c514218))
3. (tpp c514219 c514218)
4. (ec c514220 c514219)

> hyp


LEMMA

In the overlap case, exclusion of converse parthood yields po(x,z) or pp(x,z).
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (tpp y z)) & (o x z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? ((((~ (ec c520197 c520196)) v (~ (tpp c520196 c520195))) v (~ (o c520197 c520195))) v ((po c520197 c520195) v (pp c520197 c520195)))


> hypdisj
=============================
Step 3

? (pp c520197 c520195)

1. (~ (po c520197 c520195))
2. (o c520197 c520195)
3. (tpp c520196 c520195)
4. (ec c520197 c520196)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c520197 c520195)
|
|1. (~ (pp c520197 c520195))
|2. (~ (po c520197 c520195))
|3. (o c520197 c520195)
|4. (tpp c520196 c520195)
|5. (ec c520197 c520196)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c520195 c520197)
||
||1. (~ (p c520197 c520195))
||2. (~ (pp c520197 c520195))
||3. (~ (po c520197 c520195))
||4. (o c520197 c520195)
||5. (tpp c520196 c520195)
||6. (ec c520197 c520196)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c520197 c520195)
||||
||||1. (~ (p c520195 c520197))
||||2. (~ (p c520197 c520195))
||||3. (~ (pp c520197 c520195))
||||4. (~ (po c520197 c520195))
||||5. (o c520197 c520195)
||||6. (tpp c520196 c520195)
||||7. (ec c520197 c520196)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (p c520197 c520195))
|||
|||1. (~ (p c520195 c520197))
|||2. (~ (p c520197 c520195))
|||3. (~ (pp c520197 c520195))
|||4. (~ (po c520197 c520195))
|||5. (o c520197 c520195)
|||6. (tpp c520196 c520195)
|||7. (ec c520197 c520196)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c520197 c520195))
||
||1. (~ (p c520195 c520197))
||2. (~ (p c520197 c520195))
||3. (~ (pp c520197 c520195))
||4. (~ (po c520197 c520195))
||5. (o c520197 c520195)
||6. (tpp c520196 c520195)
||7. (ec c520197 c520196)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c520195 c520197))
|
|1. (~ (p c520197 c520195))
|2. (~ (pp c520197 c520195))
|3. (~ (po c520197 c520195))
|4. (o c520197 c520195)
|5. (tpp c520196 c520195)
|6. (ec c520197 c520196)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 10
|
|? (~ (p c520195 c520197))
|
|1. (pp c520195 c520197)
|2. (~ (p c520197 c520195))
|3. (~ (pp c520197 c520195))
|4. (~ (po c520197 c520195))
|5. (o c520197 c520195)
|6. (tpp c520196 c520195)
|7. (ec c520197 c520196)
|
|> ((~ (p Z X)) <-- (ec X Y) (tpp Y Z))
||=============================
||Step 11
||
||? (ec c520197 Var51)
||
||1. (p c520195 c520197)
||2. (pp c520195 c520197)
||3. (~ (p c520197 c520195))
||4. (~ (pp c520197 c520195))
||5. (~ (po c520197 c520195))
||6. (o c520197 c520195)
||7. (tpp c520196 c520195)
||8. (ec c520197 c520196)
||
||> hyp
|=============================
|Step 12
|
|? (tpp c520196 c520195)
|
|1. (p c520195 c520197)
|2. (pp c520195 c520197)
|3. (~ (p c520197 c520195))
|4. (~ (pp c520197 c520195))
|5. (~ (po c520197 c520195))
|6. (o c520197 c520195)
|7. (tpp c520196 c520195)
|8. (ec c520197 c520196)
|
|> hyp
=============================
Step 13

? (~ (p c520195 c520197))

1. (~ (pp c520197 c520195))
2. (~ (po c520197 c520195))
3. (o c520197 c520195)
4. (tpp c520196 c520195)
5. (ec c520197 c520196)

> ((~ (p Z X)) <-- (ec X Y) (tpp Y Z))
|=============================
|Step 14
|
|? (ec c520197 Var56)
|
|1. (p c520195 c520197)
|2. (~ (pp c520197 c520195))
|3. (~ (po c520197 c520195))
|4. (o c520197 c520195)
|5. (tpp c520196 c520195)
|6. (ec c520197 c520196)
|
|> hyp
=============================
Step 15

? (tpp c520196 c520195)

1. (p c520195 c520197)
2. (~ (pp c520197 c520195))
3. (~ (po c520197 c520195))
4. (o c520197 c520195)
5. (tpp c520196 c520195)
6. (ec c520197 c520196)

> hyp


LEMMA

Proper part splits into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c526588 c526587)) v ((tpp c526588 c526587) v (ntpp c526588 c526587)))


> hypdisj
=============================
Step 3

? (ntpp c526588 c526587)

1. (~ (tpp c526588 c526587))
2. (pp c526588 c526587)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f520310 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c526588 c526587)
|
|1. (~ (ntpp c526588 c526587))
|2. (~ (tpp c526588 c526587))
|3. (pp c526588 c526587)
|
|> hyp
=============================
Step 5

? (~ (ec (f520310 c526588 c526587 Var32) c526588))

1. (~ (ntpp c526588 c526587))
2. (~ (tpp c526588 c526587))
3. (pp c526588 c526587)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c526588 Var36)
||
||1. (ec (f520310 c526588 c526587 Var32) c526588)
||2. (~ (ntpp c526588 c526587))
||3. (~ (tpp c526588 c526587))
||4. (pp c526588 c526587)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f520310 c526588 c526587 Var32) c526587)
|
|1. (ec (f520310 c526588 c526587 Var32) c526588)
|2. (~ (ntpp c526588 c526587))
|3. (~ (tpp c526588 c526587))
|4. (pp c526588 c526587)
|
|> ((ec (f520310 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c526588 c526587))
||
||1. (~ (ec (f520310 c526588 c526587 Var32) c526587))
||2. (ec (f520310 c526588 c526587 Var32) c526588)
||3. (~ (ntpp c526588 c526587))
||4. (~ (tpp c526588 c526587))
||5. (pp c526588 c526587)
||
||> hyp
|=============================
|Step 9
|
|? (pp c526588 c526587)
|
|1. (~ (ec (f520310 c526588 c526587 Var32) c526587))
|2. (ec (f520310 c526588 c526587 Var32) c526588)
|3. (~ (ntpp c526588 c526587))
|4. (~ (tpp c526588 c526587))
|5. (pp c526588 c526587)
|
|> hyp
=============================
Step 10

? (~ (tpp c526588 c526587))

1. (ec (f520310 c526588 c526587 Var32) c526588)
2. (~ (ntpp c526588 c526587))
3. (~ (tpp c526588 c526587))
4. (pp c526588 c526587)

> hyp


LEMMA

Refine the overlap case to po(x,z) or tpp(x,z) or ntpp(x,z).
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (tpp y z)) & (o x z)) => ((po x z) v ((tpp x z) v (ntpp x z)))))))


> revsk
=============================
Step 2

? ((((~ (ec c533132 c533131)) v (~ (tpp c533131 c533130))) v (~ (o c533132 c533130))) v ((po c533132 c533130) v ((tpp c533132 c533130) v (ntpp c533132 c533130))))


> hypdisj
=============================
Step 3

? (ntpp c533132 c533130)

1. (~ (tpp c533132 c533130))
2. (~ (po c533132 c533130))
3. (o c533132 c533130)
4. (tpp c533131 c533130)
5. (ec c533132 c533131)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c533132 c533130)
|
|1. (~ (ntpp c533132 c533130))
|2. (~ (tpp c533132 c533130))
|3. (~ (po c533132 c533130))
|4. (o c533132 c533130)
|5. (tpp c533131 c533130)
|6. (ec c533132 c533131)
|
|> ((pp Y Z) <-- (ec Y X) (tpp X Z) (o Y Z) (~ (po Y Z)))
||||=============================
||||Step 5
||||
||||? (ec c533132 Var31)
||||
||||1. (~ (pp c533132 c533130))
||||2. (~ (ntpp c533132 c533130))
||||3. (~ (tpp c533132 c533130))
||||4. (~ (po c533132 c533130))
||||5. (o c533132 c533130)
||||6. (tpp c533131 c533130)
||||7. (ec c533132 c533131)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (tpp c533131 c533130)
|||
|||1. (~ (pp c533132 c533130))
|||2. (~ (ntpp c533132 c533130))
|||3. (~ (tpp c533132 c533130))
|||4. (~ (po c533132 c533130))
|||5. (o c533132 c533130)
|||6. (tpp c533131 c533130)
|||7. (ec c533132 c533131)
|||
|||> hyp
||=============================
||Step 7
||
||? (o c533132 c533130)
||
||1. (~ (pp c533132 c533130))
||2. (~ (ntpp c533132 c533130))
||3. (~ (tpp c533132 c533130))
||4. (~ (po c533132 c533130))
||5. (o c533132 c533130)
||6. (tpp c533131 c533130)
||7. (ec c533132 c533131)
||
||> hyp
|=============================
|Step 8
|
|? (~ (po c533132 c533130))
|
|1. (~ (pp c533132 c533130))
|2. (~ (ntpp c533132 c533130))
|3. (~ (tpp c533132 c533130))
|4. (~ (po c533132 c533130))
|5. (o c533132 c533130)
|6. (tpp c533131 c533130)
|7. (ec c533132 c533131)
|
|> hyp
=============================
Step 9

? (~ (tpp c533132 c533130))

1. (~ (ntpp c533132 c533130))
2. (~ (tpp c533132 c533130))
3. (~ (po c533132 c533130))
4. (o c533132 c533130)
5. (tpp c533131 c533130)
6. (ec c533132 c533131)

> hyp


LEMMA

Use connection transport to get c(x,z). Then split into ec(x,z) or o(x,z). In the overlap case refine to po(x,z) or pp(x,z), then split pp into tpp(x,z) or ntpp(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (tpp y z)) => ((((ec x z) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (ec c540288 c540287)) v (~ (tpp c540287 c540286))) v ((((ec c540288 c540286) v (po c540288 c540286)) v (tpp c540288 c540286)) v (ntpp c540288 c540286)))


> hypdisj
=============================
Step 3

? (ntpp c540288 c540286)

1. (~ (tpp c540288 c540286))
2. (~ (po c540288 c540286))
3. (~ (ec c540288 c540286))
4. (tpp c540287 c540286)
5. (ec c540288 c540287)

> ((ntpp Y Z) <-- (ec Y X) (tpp X Z) (o Y Z) (~ (po Y Z)) (~ (tpp Y Z)))
||||=============================
||||Step 4
||||
||||? (ec c540288 Var32)
||||
||||1. (~ (ntpp c540288 c540286))
||||2. (~ (tpp c540288 c540286))
||||3. (~ (po c540288 c540286))
||||4. (~ (ec c540288 c540286))
||||5. (tpp c540287 c540286)
||||6. (ec c540288 c540287)
||||
||||> hyp
|||=============================
|||Step 5
|||
|||? (tpp c540287 c540286)
|||
|||1. (~ (ntpp c540288 c540286))
|||2. (~ (tpp c540288 c540286))
|||3. (~ (po c540288 c540286))
|||4. (~ (ec c540288 c540286))
|||5. (tpp c540287 c540286)
|||6. (ec c540288 c540287)
|||
|||> hyp
||=============================
||Step 6
||
||? (o c540288 c540286)
||
||1. (~ (ntpp c540288 c540286))
||2. (~ (tpp c540288 c540286))
||3. (~ (po c540288 c540286))
||4. (~ (ec c540288 c540286))
||5. (tpp c540287 c540286)
||6. (ec c540288 c540287)
||
||> ((o Y Z) <-- (ec Y X) (tpp X Z) (~ (ec Y Z)))
||||=============================
||||Step 7
||||
||||? (ec c540288 Var37)
||||
||||1. (~ (o c540288 c540286))
||||2. (~ (ntpp c540288 c540286))
||||3. (~ (tpp c540288 c540286))
||||4. (~ (po c540288 c540286))
||||5. (~ (ec c540288 c540286))
||||6. (tpp c540287 c540286)
||||7. (ec c540288 c540287)
||||
||||> hyp
|||=============================
|||Step 8
|||
|||? (tpp c540287 c540286)
|||
|||1. (~ (o c540288 c540286))
|||2. (~ (ntpp c540288 c540286))
|||3. (~ (tpp c540288 c540286))
|||4. (~ (po c540288 c540286))
|||5. (~ (ec c540288 c540286))
|||6. (tpp c540287 c540286)
|||7. (ec c540288 c540287)
|||
|||> hyp
||=============================
||Step 9
||
||? (~ (ec c540288 c540286))
||
||1. (~ (o c540288 c540286))
||2. (~ (ntpp c540288 c540286))
||3. (~ (tpp c540288 c540286))
||4. (~ (po c540288 c540286))
||5. (~ (ec c540288 c540286))
||6. (tpp c540287 c540286)
||7. (ec c540288 c540287)
||
||> hyp
|=============================
|Step 10
|
|? (~ (po c540288 c540286))
|
|1. (~ (ntpp c540288 c540286))
|2. (~ (tpp c540288 c540286))
|3. (~ (po c540288 c540286))
|4. (~ (ec c540288 c540286))
|5. (tpp c540287 c540286)
|6. (ec c540288 c540287)
|
|> hyp
=============================
Step 11

? (~ (tpp c540288 c540286))

1. (~ (ntpp c540288 c540286))
2. (~ (tpp c540288 c540286))
3. (~ (po c540288 c540286))
4. (~ (ec c540288 c540286))
5. (tpp c540287 c540286)
6. (ec c540288 c540287)

> hyp
